(set-logic QF_BV)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(push 1)
(assert (= v0 v1 v0 v6 v1 v4 v3 v0))
(declare-const v7 Bool)
(pop 1)
(push 1)
(assert (= v3 v3 v4 v6 v3))
(declare-const bv_24-0 (_ BitVec 24))
(assert v2)
(assert v6)
(declare-const v8 Bool)
(assert (=> v2 v0))
(assert v1)
(assert (bvult bv_24-0 bv_24-0))
(pop 1)
(declare-const bv_3-0 (_ BitVec 3))
(declare-const v9 Bool)
(assert v9)
(declare-const v10 Bool)
(push 1)
(declare-const v11 Bool)
(declare-const v12 Bool)
(assert v5)
(push 1)
(declare-const v13 Bool)
(assert (=> (distinct (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0) (bvsrem bv_3-0 (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0)) bv_3-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))))
(assert v4)
(assert (=> (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) v4))
(assert (or v12 (bvult bv_3-0 (bvnor bv_3-0 bv_3-0)) v9 v5 (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) v9 (=> (distinct (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0) (bvsrem bv_3-0 (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0)) bv_3-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))))
(pop 1)
(declare-const v14 Bool)
(pop 1)
(declare-const bv_7-0 (_ BitVec 7))
(assert (= (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0) bv_3-0 (bvnor bv_3-0 bv_3-0)))
(push 1)
(push 1)
(assert v3)
(check-sat)
(pop 1)
(declare-const v15 Bool)
(assert (bvult bv_3-0 (bvnor bv_3-0 bv_3-0)))
(assert (xor (or (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2) (distinct bv_3-0 (bvnor bv_3-0 bv_3-0) (bvnor bv_3-0 bv_3-0) bv_3-0) v10 (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2) v5 v5 v10 v0 (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) v4 (bvult bv_3-0 (bvnor bv_3-0 bv_3-0))) (not v0) (not v0) v3 v4 v0 (= (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0) bv_3-0 (bvnor bv_3-0 bv_3-0))))
(pop 1)
(declare-const v16 Bool)
(assert v6)
(assert v9)
(declare-const bv_27-0 (_ BitVec 27))
(declare-const v17 Bool)
(assert (bvule (bvnor bv_3-0 bv_3-0) bv_3-0))
(declare-const v18 Bool)
(assert v3)
(push 1)
(declare-const v19 Bool)
(assert (and v16 v9 v16 v3))
(declare-const v20 Bool)
(push 1)
(declare-const v21 Bool)
(assert (xor (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)) (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) (and v16 v9 v16 v3) (or (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2) (distinct bv_3-0 (bvnor bv_3-0 bv_3-0) (bvnor bv_3-0 bv_3-0) bv_3-0) v10 (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2) v5 v5 v10 v0 (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) v4 (bvult bv_3-0 (bvnor bv_3-0 bv_3-0))) v19 v9 v0))
(check-sat)
(assert v6)
(declare-const v22 Bool)
(assert (=> (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))))
(assert (or (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) v1 v0 v17 (xor (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)) (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) (and v16 v9 v16 v3) (or (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2) (distinct bv_3-0 (bvnor bv_3-0 bv_3-0) (bvnor bv_3-0 bv_3-0) bv_3-0) v10 (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2) v5 v5 v10 v0 (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) v4 (bvult bv_3-0 (bvnor bv_3-0 bv_3-0))) v19 v9 v0) (distinct (bvshl #b01110000 #b01110000) (bvshl #b01110000 #b01110000) #b01110000 #b01110000 (bvshl #b01110000 #b01110000)) (xor (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)) (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) (and v16 v9 v16 v3) (or (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2) (distinct bv_3-0 (bvnor bv_3-0 bv_3-0) (bvnor bv_3-0 bv_3-0) bv_3-0) v10 (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2) v5 v5 v10 v0 (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) v4 (bvult bv_3-0 (bvnor bv_3-0 bv_3-0))) v19 v9 v0) v10 v10))
(assert (=> v18 (or (and v16 v9 v16 v3) (distinct (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (concat bv_3-0 bv_3-0) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v6)))
(declare-const v23 Bool)
(declare-const bv_12-0 (_ BitVec 12))
(push 1)
(assert (not v16))
(push 1)
(declare-const v24 Bool)
(pop 1)
(declare-const v25 Bool)
(assert (= (= (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0) bv_3-0 (bvnor bv_3-0 bv_3-0)) (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (=> (=> v18 (or (and v16 v9 v16 v3) (distinct (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (concat bv_3-0 bv_3-0) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v6)) (= (=> (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) (distinct (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (concat bv_3-0 bv_3-0) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v6 (distinct (bvshl #b01110000 #b01110000) (bvshl #b01110000 #b01110000) #b01110000 #b01110000 (bvshl #b01110000 #b01110000)) (and v16 v9 v16 v3) v16 (= bv_27-0 bv_27-0 (bvor bv_27-0 bv_27-0)) v1 (= (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0) bv_3-0 (bvnor bv_3-0 bv_3-0)) v10)) v0 v0 v3 (=> v18 (or (and v16 v9 v16 v3) (distinct (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (concat bv_3-0 bv_3-0) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v6)) v20 (distinct (bvshl #b01110000 #b01110000) (bvshl #b01110000 #b01110000) #b01110000 #b01110000 (bvshl #b01110000 #b01110000)) v21))
(assert (distinct (= (concat #x1c #x1c) (concat #x1c #x1c) (concat #x1c #x1c)) v16 v6 (= (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0) bv_3-0 (bvnor bv_3-0 bv_3-0)) v6 (distinct (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (concat bv_3-0 bv_3-0) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)))))
(declare-const v26 Bool)
(declare-const v27 Bool)
(assert (or (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2) (distinct bv_3-0 (bvnor bv_3-0 bv_3-0) (bvnor bv_3-0 bv_3-0) bv_3-0) v10 (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2) v5 v5 v10 v0 (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) v4 (bvult bv_3-0 (bvnor bv_3-0 bv_3-0))))
(declare-const v28 Bool)
(pop 1)
(assert (= v20 (= (bvor bv_27-0 bv_27-0) (bvor bv_27-0 bv_27-0) bv_27-0)))
(assert (xor (and v16 v9 v16 v3) (= (bvor bv_27-0 bv_27-0) (bvor bv_27-0 bv_27-0) bv_27-0) v4))
(push 1)
(pop 1)
(assert (= (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) v16 v0 v3 (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (not v19) v9))
(pop 1)
(declare-const v29 Bool)
(push 1)
(push 1)
(assert (or (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v0))
(assert v10)
(declare-const v30 Bool)
(assert (= (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) v1 (= (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0) bv_3-0 (bvnor bv_3-0 bv_3-0)) v9 v3 v1 v6 v3 v29 (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)))))
(declare-const v31 Bool)
(pop 1)
(assert (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))))
(declare-const v32 Bool)
(declare-const bv_3-4 (_ BitVec 3))
(assert v29)
(declare-const v33 Bool)
(declare-const v34 Bool)
(declare-const v35 Bool)
(check-sat)
(assert v2)
(declare-const v36 Bool)
(declare-const v37 Bool)
(assert v3)
(push 1)
(declare-const v38 Bool)
(declare-const v39 Bool)
(assert (xor v16 v5))
(declare-const v40 Bool)
(assert v10)
(assert (= (= (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) v1 (= (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0) bv_3-0 (bvnor bv_3-0 bv_3-0)) v9 v3 v1 v6 v3 v29 (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)))) (distinct bv_3-0 (bvnor bv_3-0 bv_3-0) (bvnor bv_3-0 bv_3-0) bv_3-0) (= (bvor bv_27-0 bv_27-0) (bvor bv_27-0 bv_27-0) bv_27-0) (distinct (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (concat bv_3-0 bv_3-0) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v38 (xor v16 v5) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (xor v16 v5)))
(assert (= (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0) bv_3-0 (bvnor bv_3-0 bv_3-0)))
(declare-const v41 Bool)
(assert (and (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2) v3 (=> (= (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0) bv_3-0 (bvnor bv_3-0 bv_3-0)) (distinct bv_3-0 (bvnor bv_3-0 bv_3-0) (bvnor bv_3-0 bv_3-0) bv_3-0)) v1 v19 (=> v17 v10) (distinct (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) (distinct (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (concat bv_3-0 bv_3-0) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v37 v9) v1 (xor v16 v5) v41))
(declare-const v42 Bool)
(declare-const bv_30-0 (_ BitVec 30))
(assert (not (xor v16 v5)))
(declare-const v43 Bool)
(declare-const bv_29-0 (_ BitVec 29))
(declare-const v44 Bool)
(assert (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2))
(assert (= (and v16 v9 v16 v3) v39 v41 (or (or v5 (= #b01110000 #b01110000 (bvshl #b01110000 #b01110000) (bvshl #b01110000 #b01110000)) (and v16 v9 v16 v3) v16) v6 (= (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0) bv_3-0 (bvnor bv_3-0 bv_3-0))) (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v17 (=> (= v5 v2 v3 v4 v2 v2 v6) v18)))
(declare-const v45 Bool)
(declare-const v46 Bool)
(declare-const bv_7-4 (_ BitVec 7))
(assert (distinct (and v16 v9 v16 v3) (and v16 v9 v16 v3) v9 (and (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2) v3 (=> (= (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0) bv_3-0 (bvnor bv_3-0 bv_3-0)) (distinct bv_3-0 (bvnor bv_3-0 bv_3-0) (bvnor bv_3-0 bv_3-0) bv_3-0)) v1 v19 (=> v17 v10) (distinct (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) (distinct (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (concat bv_3-0 bv_3-0) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v37 v9) v1 (xor v16 v5) v41) (distinct (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) (distinct (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (concat bv_3-0 bv_3-0) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v37 v9) (distinct (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (concat bv_3-0 bv_3-0) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)))))
(check-sat)
(declare-const v47 Bool)
(declare-const bv_30-1 (_ BitVec 30))
(declare-const v48 Bool)
(pop 1)
(declare-const v49 Bool)
(assert (= v6 v0 (= (bvor bv_27-0 bv_27-0) (bvor bv_27-0 bv_27-0) bv_27-0) v20 v49))
(declare-const v50 Bool)
(check-sat)
(push 1)
(declare-const v51 Bool)
(declare-const v52 Bool)
(assert (and (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v29 (or (= #b01110000 #b01110000 (bvshl #b01110000 #b01110000) (bvshl #b01110000 #b01110000)) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)) (=> (= v5 v2 v3 v4 v2 v2 v6) v18) (= bv_7-0 (bvudiv bv_7-0 bv_7-0) (_ bv72 7)) v16 (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v5) v3))
(declare-const v53 Bool)
(assert (and (= bv_7-0 (bvudiv bv_7-0 bv_7-0) (_ bv72 7)) v33 (or (= #b01110000 #b01110000 (bvshl #b01110000 #b01110000) (bvshl #b01110000 #b01110000)) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)) (=> (= v5 v2 v3 v4 v2 v2 v6) v18) (= bv_7-0 (bvudiv bv_7-0 bv_7-0) (_ bv72 7)) v16 (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v5) v29 (or (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)) (= (_ bv316 9) (_ bv316 9)) v4) (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v6 (= bv_3-0 (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0))))
(declare-const v54 Bool)
(assert (distinct (and (= bv_7-0 (bvudiv bv_7-0 bv_7-0) (_ bv72 7)) v33 (or (= #b01110000 #b01110000 (bvshl #b01110000 #b01110000) (bvshl #b01110000 #b01110000)) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)) (=> (= v5 v2 v3 v4 v2 v2 v6) v18) (= bv_7-0 (bvudiv bv_7-0 bv_7-0) (_ bv72 7)) v16 (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v5) v29 (or (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)) (= (_ bv316 9) (_ bv316 9)) v4) (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v6 (= bv_3-0 (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0))) (and (= bv_7-0 (bvudiv bv_7-0 bv_7-0) (_ bv72 7)) v33 (or (= #b01110000 #b01110000 (bvshl #b01110000 #b01110000) (bvshl #b01110000 #b01110000)) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)) (=> (= v5 v2 v3 v4 v2 v2 v6) v18) (= bv_7-0 (bvudiv bv_7-0 bv_7-0) (_ bv72 7)) v16 (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v5) v29 (or (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)) (= (_ bv316 9) (_ bv316 9)) v4) (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v6 (= bv_3-0 (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0))) (=> v17 v10)))
(push 1)
(declare-const bv_20-0 (_ BitVec 20))
(assert (and (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v29 (or (= #b01110000 #b01110000 (bvshl #b01110000 #b01110000) (bvshl #b01110000 #b01110000)) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)) (=> (= v5 v2 v3 v4 v2 v2 v6) v18) (= bv_7-0 (bvudiv bv_7-0 bv_7-0) (_ bv72 7)) v16 (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v5) v3))
(assert (= (and (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v29 (or (= #b01110000 #b01110000 (bvshl #b01110000 #b01110000) (bvshl #b01110000 #b01110000)) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)) (=> (= v5 v2 v3 v4 v2 v2 v6) v18) (= bv_7-0 (bvudiv bv_7-0 bv_7-0) (_ bv72 7)) v16 (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v5) v3) (= (_ bv316 9) (_ bv316 9)) (distinct (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (concat bv_3-0 bv_3-0) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v33 (= (_ bv443 9) (_ bv443 9) (_ bv443 9) (_ bv443 9) (_ bv443 9)) (and (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v29 (or (= #b01110000 #b01110000 (bvshl #b01110000 #b01110000) (bvshl #b01110000 #b01110000)) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)) (=> (= v5 v2 v3 v4 v2 v2 v6) v18) (= bv_7-0 (bvudiv bv_7-0 bv_7-0) (_ bv72 7)) v16 (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v5) v3)))
(assert v37)
(declare-const v55 Bool)
(check-sat)
(assert v36)
(assert (=> (= (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0) bv_3-0 (bvnor bv_3-0 bv_3-0)) (distinct bv_3-0 (bvnor bv_3-0 bv_3-0) (bvnor bv_3-0 bv_3-0) bv_3-0)))
(assert (= v0 (or v5 (= #b01110000 #b01110000 (bvshl #b01110000 #b01110000) (bvshl #b01110000 #b01110000)) (and v16 v9 v16 v3) v16) (bvult bv_3-0 (bvnor bv_3-0 bv_3-0)) (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v51 (= (and (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v29 (or (= #b01110000 #b01110000 (bvshl #b01110000 #b01110000) (bvshl #b01110000 #b01110000)) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)) (=> (= v5 v2 v3 v4 v2 v2 v6) v18) (= bv_7-0 (bvudiv bv_7-0 bv_7-0) (_ bv72 7)) v16 (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v5) v3) (= (_ bv316 9) (_ bv316 9)) (distinct (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0)) (concat bv_3-0 bv_3-0) (bvsub (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v33 (= (_ bv443 9) (_ bv443 9) (_ bv443 9) (_ bv443 9) (_ bv443 9)) (and (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v29 (or (= #b01110000 #b01110000 (bvshl #b01110000 #b01110000) (bvshl #b01110000 #b01110000)) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0)) (=> (= v5 v2 v3 v4 v2 v2 v6) v18) (= bv_7-0 (bvudiv bv_7-0 bv_7-0) (_ bv72 7)) v16 (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) (= v17 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct bv_7-0 bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0) bv_7-0 (bvxor bv_7-0 bv_7-0 bv_7-0))) (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v5) v3)) (=> (= (bvmul (bvnor bv_3-0 bv_3-0) bv_3-0) bv_3-0 (bvnor bv_3-0 bv_3-0)) (distinct bv_3-0 (bvnor bv_3-0 bv_3-0) (bvnor bv_3-0 bv_3-0) bv_3-0)) v33 (and v16 v9 v16 v3) (bvule (bvnor bv_3-0 bv_3-0) bv_3-0) v29))
(declare-const bv_29-0 (_ BitVec 29))
(declare-const v56 Bool)
(assert v3)
(declare-const v57 Bool)
(assert v9)
(pop 1)
(declare-const v58 Bool)
(assert (and (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) v33 (= (_ bv443 9) (_ bv443 9) (_ bv443 9) (_ bv443 9) (_ bv443 9)) (= v4 v10 (= bv_27-0 bv_27-0 bv_27-0 bv_27-0) (distinct (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0) (concat bv_3-0 bv_3-0))) (=> v17 v10) (or v1 v10 v4 v5 v3 v10 v10 v5 v0 v2) v2 v52 (= (bvxor ((_ extract 5 1) (bvxor bv_7-0 bv_7-0 bv_7-0)) ((_ extract 5 1) (bvxor bv_7-0 bv_7-0 bv_7-0))) ((_ extract 5 1) (bvxor bv_7-0 bv_7-0 bv_7-0)) (bvxor ((_ extract 5 1) (bvxor bv_7-0 bv_7-0 bv_7-0)) ((_ extract 5 1) (bvxor bv_7-0 bv_7-0 bv_7-0))) ((_ extract 5 1) (bvxor bv_7-0 bv_7-0 bv_7-0)) (bvxor ((_ extract 5 1) (bvxor bv_7-0 bv_7-0 bv_7-0)) ((_ extract 5 1) (bvxor bv_7-0 bv_7-0 bv_7-0))))))
(declare-const bv_6-2 (_ BitVec 6))
(check-sat)
